Nuprl Definition : chain_master_ind
11,40
postcript
pdf
case
x
of
config(
list
) =>
config
(
list
)
c
seq(
from
,
to
,
num
) =>
seq
(
from
;
to
;
num
)
== case
x
of inl(
x
) =>
config
(
x
) | inr(
x
) =>
seq
(
x
.1;(
x
.2).1;
x
.2.2)
latex
Definitions
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
t
.1
,
t
.2
FDL editor aliases
chain_master_ind
origin